\begin{tabbing}
$\forall$\=$E$:Type, ${\it eq}$:EqDecider($E$), $T$:(Id$\rightarrow$Id$\rightarrow$Type), $V$:(Knd$\rightarrow$Id$\rightarrow$Type),\+
\\[0ex]${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))), ${\it pred?}$:($E$$\rightarrow$(?$E$)),
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))), ${\it when}$, ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow\mathbb{Q}\rightarrow$$T$(loc($e$),$x$)), ${\it time}$:($E$$\rightarrow\mathbb{Q}$),
\\[0ex]$p$:SESAxioms\{i:l\}($E$;$T$;${\it pred?}$;${\it info}$;${\it when}$;${\it after}$;${\it time}$).
\-\\[0ex]ESAxioms\{i:l\}($E$;$T$;$\lambda$$l$,${\it tg}$. $V$(rcv($l$,${\it tg}$),destination($l$));$\lambda$$e$.loc($e$);$\lambda$$e$.
\\[0ex]kind($e$);${\it val}$;${\it when}$;${\it after}$;${\it time}$;$\lambda$$l$,$e$. sends(${\it eq}$;IdLnkDeq;${\it pred?}$;${\it info}$;${\it val}$;$p$.1;$e$;$l$);$\lambda$$e$.
\\[0ex]sender($e$);$\lambda$$e$.index(${\it eq}$;IdLnkDeq;${\it pred?}$;${\it info}$;$p$.1;$e$);$\lambda$$e$.first($e$);$\lambda$$e$.pred($e$);$\lambda$$e$,${\it e'}$. $e$ $<$ ${\it e'}$)
\end{tabbing}